In the field of computer software testing, different approaches have been developed to more accurately and completely test program function. For example, program modeling and model checking allow certain kinds of debugging analysis that may not otherwise be possible or practical in direct analysis of a program.
The state space of a program is the set of possible states that a program can potentially be in while it is executing. For most non-trivial programs, the state space is very large and difficult, if not impossible, to test exhaustively. Program models simplify certain aspects of programs to reduce the state space that needs to be explored to detect errors in the program, and such models therefore facilitate more complete testing of the overall behavior of programs. Program models can be used to analyze programs as a whole, or, for larger programs, to analyze them one part at a time. When errors are found, changes can then be made to the program source code to correct the errors.
Concurrent (or, multithreaded) programs have two or more program threads that can execute at the same time. In a concurrent program, one program thread can perform actions that affect other threads (e.g., by affecting a program variable that is used by another thread). Even when the execution of one thread in isolation results in no errors, the concurrent execution of another thread may affect the first thread (or vice versa) and result in an error that was previously hidden. An interaction between threads is called an interleaving. The number of possible interleavings between threads can expand the state space of a concurrent program well beyond the state space of individual threads. Therefore, concurrent programs present additional challenges in terms of error detection and modeling program behavior.
Partial-order reduction techniques have been developed that reduce the state space of a concurrent program in order to allow error checking in a concurrent program that would otherwise have a state space too big to be explored completely. Partial-order reduction techniques work by delaying execution of some threads in order to reduce the number of interleavings between threads. For example, if a program consists of two threads, t1 and t2, the state space of thread t1 can be explored while the execution of thread t2 is delayed. As long as thread t2 is eventually executed, the program can still be accurately modeled.
In some cases, threads enter loops, or cycles, from which they do not exit. In the context of modeling concurrent programs, this gives rise to a condition known as the ignoring problem. For example, if the execution of thread t1 is explored while the execution of thread t2 is delayed, and thread t1 enters a loop from which t2 can never be executed, the execution of thread t2 is delayed indefinitely and cannot be properly tested. If thread t2 is delayed indefinitely, errors that occur during the execution of thread t2 may not be discovered, making the partial-order reduction algorithm unsound.
Cycle detection is one way of dealing with the ignoring problem in partial-order reduction. In partial-order reduction techniques that use cycle detection, whenever a cycle is detected in a thread that is being explored, the detected cycle is closed and other threads in the program are then scheduled to be executed. FIGS. 1 and 2 illustrate a partial-order reduction technique with cycle detection in a concurrent program with two threads, t1 and t2. In FIG. 1, thread t1 is being explored while thread t2 is postponed. The execution of thread t1 includes a path 150 that leads to cycle 170, and a path 160 that does not lead to a cycle. Cycle detection 110 is used to schedule execution of thread t2 when cycle 170 in thread t1 is detected, thereby avoiding the ignoring problem. In FIG. 2, the execution of thread t1 includes a path 250 that leads to cycle 270, and a path 260 that leads to cycle 280. In FIG. 2, cycle detection 210 is used to schedule execution of thread t2 when cycles 270 and 280 in thread t1 are detected.
As illustrated in FIGS. 1 and 2, prior partial-order reduction techniques avoid the ignoring problem with cycle detection, but add scheduled thread executions at detected cycles.
Whatever the benefits of prior techniques, they do not have the advantages of the following techniques and tools.